| 1: | le(0,y) | → true | |
| 2: | le(s(x),0) | → false | |
| 3: | le(s(x),s(y)) | → le(x,y) | |
| 4: | pred(s(x)) | → x | |
| 5: | minus(x,0) | → x | |
| 6: | minus(x,s(y)) | → pred(minus(x,y)) | |
| 7: | mod(0,y) | → 0 | |
| 8: | mod(s(x),0) | → 0 | |
| 9: | mod(s(x),s(y)) | → if_mod(le(y,x),s(x),s(y)) | |
| 10: | if_mod(true,s(x),s(y)) | → mod(minus(x,y),s(y)) | |
| 11: | if_mod(false,s(x),s(y)) | → s(x) | |
| 12: | LE(s(x),s(y)) | → LE(x,y) | |
| 13: | MINUS(x,s(y)) | → PRED(minus(x,y)) | |
| 14: | MINUS(x,s(y)) | → MINUS(x,y) | |
| 15: | MOD(s(x),s(y)) | → IF_MOD(le(y,x),s(x),s(y)) | |
| 16: | MOD(s(x),s(y)) | → LE(y,x) | |
| 17: | IF_MOD(true,s(x),s(y)) | → MOD(minus(x,y),s(y)) | |
| 18: | IF_MOD(true,s(x),s(y)) | → MINUS(x,y) | |